Nuprl Lemma : member-remove-repeats
11,40
postcript
pdf
T
:Type,
eq
:EqDecider(
T
),
L
:(
T
List),
a
:
T
. (
a
remove-repeats(
eq
;
L
))
(
a
L
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
type
List
,
[]
,
left
+
right
,
prop{i:l}
,
P
Q
,
l-union(
eq
;
as
;
bs
)
,
x
:
A
B
(
x
)
,
P
Q
,
P
Q
,
x
:
A
B
(
x
)
,
P
Q
,
P
Q
,
remove-repeats(
eq
;
L
)
,
Type
,
EqDecider(
T
)
,
guard(
T
)
,
False
Lemmas
nil
member
,
deq
wf
,
iff
functionality
wrt
iff
,
member-union
,
l-union
wf
,
l
member
wf
origin
T:Type, eq:EqDecider(T), L:(T List), a:T. (a 
remove-repeats(eq; L)) 
(a L) T:Type, eq:EqDecider(T), L:(T List), a:T. (a remove-repeats(eq; L)) (a L) Tx:A. B(x) l)
Q
B(x) Q Q
B(x)
Q Q